-- -*- haskell -*-

module RPTypes where

import Data.Sequence as Sequence
import Maybe

import Data.Set as Set
import Data.Word

import Foreign.C.Types

-- import Debug.Trace
-- import Debug.Trace.Location

type UnsignedNum = Int

randSeedDefault = 103010010 :: Int -- for inout test 100 means last=out, 102 last = in

allSolutions = True  -- calculate all soultions in inductive phase

stacksize = 800000 :: UnsignedNum
trailsize = 20000 :: UnsignedNum
-- stacksize = 10000 :: UnsignedNum
argRegSize = 40 :: UnsignedNum -- number of argument registers

debug=True
debugdump=False
printTree =False

trialCount = 0 :: Int -- 0 => 1 trial
indTrialCountDefault = 0 :: Int

treeDepth = 10 :: Int

dumpWidth = 18 :: Int

-- restartThresholdDefault = 1500000000 :: Word64 
-- restartThresholdDefault = 30000000 :: Word64 

-- We ned c2hs just for the next bit (Counters)
#c
#include <stdint.h>
#endc

type Counter = {# type uint64_t #}

instCountMax = 30000000001 :: Counter

-- shortThreshold = 200000000 :: Word64 
shortThresholdDefault = 10000000:: Counter

-- shortThreshold = 100000:: Word64
restartThresholdDefault = shortThresholdDefault :: Counter

pointChangeDefault = 0 :: UnsignedNum

-- next now unused
-- minimumRestartThreshold = RPTypes.restartThresholdDefault `div` 2 ---

restartThresholdScale = 1.0

weightScalePowerDefault = 6 :: Double

weightAdd = 0 :: Double

lambdaDefault = 0.60::Double 

printPossibleWitnesses = True  -- enables output

exceptOnNoPredicate = True -- exception if no predicate in "call"

randomCallStackOnly = True -- only push randomized clauses onto the call stack



-- histDepth = 5

alwaysContinue = False -- don't prompt to continue, Just Do It^{TM}


{- PQueue is a Queue with a lookahead function, "peekPQueue" -}
data PQueue a = PQ (Seq a) (Maybe a) 

data Term = T {atom::Atom, arity::Arity, args::[Term], tpos::Position}  -- standard term
	  | I Int Position  -- integer
	  | F Double Position -- floating
	  | V Variable Position -- variable
	  | L ListTerm Position
	  | CutTerm Position
	  | NullTerm 
          deriving (Eq)

isCutTerm (CutTerm _) = True
isCutTerm _ = False

getTPos :: Term -> Position
getTPos (T _ _ _ p) = p
getTPos (I _ p) = p
getTPos (F _ p) = p
getTPos (V _ p) = p
getTPos (L _ p) = p
getTPos (CutTerm p) = p
getTPos NullTerm = nullpos

data ListTerm = LE Term ListTerm
	      | LNil
	      | LTerm Term
	      deriving(Eq)

type Variable = String

cutVariable = ""::Variable -- Special variable to represent a cut which must not occur elsewhere
-- this is pretty broken and depends on never defining a null variable; but is
-- quicker than making a propoer variable type 

type Atom = String

type Arity = Word32

data Predicate = PRED { predid :: PredID,
                        clauselist :: [Clause],
                        randomized :: Bool,
                        uwrandom::Bool}
    deriving Show

data PredID = PID Atom Arity | NullPID
    deriving (Eq,Ord,Show)
    
predID :: Term -> PredID
predID (T at ar _ _) = PID at ar

clauseIDToPredID :: ClauseID -> PredID
clauseIDToPredID (CID at ar _) = (PID at ar)
clauseIDToPredID NullCID = NullPID
clauseIDToPredID ExceptCID = NullPID

data TokSymb = TokStr {string::String}  -- string starting with lower case
    | TokVar String           -- string starting with upper case
    | TokInt Int
    | TokFloat Double
    | TokNeck
    | TokOpenBrak
    | TokCloseBrak
    | TokOpenSqBrak
    | TokListRest
    | TokCloseSqBrak
    | TokComma
    | TokSemiColon
    | TokPeriod
    | TokCut
    | TokEOF
    | TokUnknown {string::String}
  deriving (Eq, Show)

data Position = POS {linenum::Int, charpos::Int, filename::String}

makePos l c f = POS l c f

data Token = TKN Position TokSymb
  deriving (Eq)
-- newtype Token = TKN (Position, TokSymb)

getTokPos (TKN p _) = p

data ClauseID = CID Atom Arity Int |
                NullCID |
                ExceptCID |
		DedCID |
		IndCID
  deriving (Eq,Show,Ord)
--
-- DIR == compiler directive
--

data Clause = CLA Term CBody |
              DIR Term
    deriving (Eq)

data Quantifier = Exists |
                  Forall
    deriving (Eq,Show)

dualQuantifier Exists = Forall
dualQuantifier Forall = Exists

-- an intermediate form for manipulating clause bodies

data Frees = Notset |
             LV (Set Term)
           deriving (Eq)

data CBody = CCONJ CBody CBody Frees |
             CDISJ CBody CBody Frees |
             CQUANT [Set Term] CBody Frees | --- `Term' elt is list of variables; existentials first, then universals, etc.  universal quantifier has empty start
             CTERM Term Frees |
             CNOT CBody Frees |
             CNIL
    deriving (Eq)

nullpos = (POS {linenum=0, charpos=0, filename=""})

type TokenQ = PQueue Token

data ParseData = PD { queue :: TokenQ,
                      clauses :: [Clause],
                      lastterm :: Maybe Term }

data PosChar = POSCHAR { ch::Char, pos::Position}

type PosString = [PosChar]

-- IF EDITING THERE IS AN EFFICIENCY HACK IN Engine.hs
inductiveCount = 0 :: Int
deductiveCount = 1 :: Int
globalCount = 2 :: Int
countCount = 3 :: Int -- Number of counters

--
-- Queue with 1 lookahead, based on existing queue; modified for the new sequence class
--

emptyPQueue :: PQueue a
addToPQueue :: PQueue a -> a -> PQueue a
dePQueue :: PQueue a -> Maybe (a, PQueue a)
peekPQueue :: PQueue a -> Maybe a
-- listToPQueue :: [a] -> PQueue a
-- pQueueToList :: PQueue a -> [a]

emptyPQueue = PQ (Sequence.empty) Nothing
addToPQueue (PQ q e) ne
    | isNothing e = (PQ (Sequence.empty) (Just ne))
    | otherwise = (PQ (q |> ne) e)
                             
dePQueue (PQ q Nothing) = Nothing
dePQueue (PQ q e) = if isNothing (deQueue q)
                       then Just (fromJust e,(PQ (Sequence.empty) Nothing))
                       else Just (fromJust e,(PQ nq (Just ne)))
                    where (ne,nq) = fromJust (deQueue q)

peekPQueue (PQ _ e) = e

deQueue :: Seq a -> Maybe (a,Seq a)
deQueue s = if not $ Sequence.null s
               then Just (index s 0,Sequence.drop 1 s)
               else Nothing

--
-- Some printing functions
--

instance Show Clause where
	show (CLA t CNIL) = (show t) ++ "."
	show (CLA t mt) = (show t) ++ " :- " ++ (show mt) ++ "."
	show (DIR t) = "DIRECTIVE: " ++ (show t) ++ "."

instance Show ListTerm where
    show LNil = "[]"
    show (LE t x) = "[" ++ (show t) ++ lint x ++ "]"
	     where lint (LE t e) = "," ++ (show t) ++ (lint e)
		   lint (LNil) = ""
		   lint (LTerm t) = "|" ++ (show t)

instance Show Term where
     show (I i _) = show i
     show (V s _) = s
     show (L tl _) = show tl
     show (T "." 2 [a,b] _) = "[" ++ (show a) ++ (listint b) -- comment out for . notation
     show (T a 0 [] _) = a
     show (T a _ ts _) = a ++ "(" ++ (pprint ts) ++ ")"
     show (CutTerm _) = "!"
     show (NullTerm) = "NULL"

instance Ord Term where
    compare (T at1 ar1 _ _) (T at2 ar2 _ _) = 
       if (at1 < at2)
         then LT
         else if (at1 > at2)
                then GT
                else (compare ar1 ar2)
    compare (T _ _ _ _) (V _ _) = GT
    compare (V _ _) (T _ _ _ _) = LT
    compare (V x _) (V y _) = compare x y
    compare NullTerm NullTerm =  EQ
    compare _ NullTerm = GT
    compare NullTerm _ = LT 

listint (T "[]" 0 [] _) = "]"
listint (T "." 2 [a,b] _) = "," ++ (show a) ++ (listint b)
listint x = "|" ++ (show x) ++ "]"

instance Show CBody where
    show (CCONJ a b f) = "(" ++ (show a) ++ "," ++ (show b) ++ ")" ++ (show f)
    show (CDISJ a b f) = "( " ++ (show a) ++ " ; " ++ (show b) ++  " )" ++ (show f)
    show (CTERM t f) = "*" ++ (show t) ++ "*" ++ (show f)
    show (CQUANT e b f) = "QUANT e-f-e-...: " ++ (show e) ++ " -- ( " ++ (show b) ++ " ) " ++ (show f)
    show (CNOT b f) = "NOT( " ++ (show b) ++ " ) " ++ (show f)
    show CNIL = "" 

fv (LV v) = v
fv Notset = Set.empty

freevars :: CBody -> Set Term
freevars (CCONJ a b f) = fv f
freevars (CDISJ a b f) = fv f
freevars (CTERM t f) = fv f
freevars (CQUANT e b f) = fv f
freevars (CNOT b f) = fv f
freevars CNIL = Set.empty

instance Show Frees where
    show Notset = " -- {NS}"
    show (LV v) = " -- {" ++ (show v) ++ "}"

blength :: CBody -> Int
blength (CCONJ x y _) = 1 + blength y
blength CNIL = 0
blength _ = 1

pprint [t] = show t
pprint (t:ts) = (show t) ++ "," ++ (pprint ts)

instance Show Token where
	show (TKN p s) = "(Token " ++ (show p) ++ " " ++ (show s) ++ ")"

instance Show Position where 
	show (POS i1 i2 f) = "Pos " ++ (show i1) ++ " " ++ (show i2)

instance Show PosChar where
    show (POSCHAR c p) = "(PosChar " ++ (show c) ++ " " ++ (show p) ++ ")"

instance (Show a) => Show (PQueue a) where
    show x = printPQ x

printPQ :: (Show a) => (PQueue a) -> String
printPQ (PQ q a) 
      | isNothing a = "***"
      | otherwise = (show $ fromJust a) ++ " , " ++  (printQ q) 

printQ :: (Show a) => (Seq a) -> String
printQ q 
         | isNothing ans = " *** "
         | otherwise = (show $ e) ++ " , " ++ printQ nq
      where ans = deQueue q
            (e,nq) = fromJust ans 

instance Eq Position where

-- mtrace b = trace ("MTRACE " ++ (show b)) b
-- etrace:: (Show a) => String -> a -> a
-- etrace s v = (trace $! ("ETRACE " ++ s ++ ": " ++ (show v))) $! v


